[[Set theory MOC]]
# Choice function

A **choice function** $f : X \rightarrowtail \bigcup X$ on a set of inhabited sets $X$ is a [[function]] which “chooses” an element from each set $A \in X$, #m/def/set i.e.
$$
\begin{align*}
(\forall A \in X)[f(A) \in A]
\end{align*}
$$
Within [[ZF]], a choice function cannot be guaranteed unless an explicit rule can be given for choosing elements, e.g. the smallest element of [[Well ordering|well ordered]] sets.
To guarantee the existence of a choice function for an arbitrary set of inhabited sets, the [[Axiom of Choice]] is required.

#
---
#state/tidy | #lang/en | #SemBr